a, b:. a < b  -(b) < -(a) 

latex

Definitions	A, {T}, T, r - s, x. t(x), True, P  Q, P  Q, P  Q, P & Q, P  Q, x:A. B(x), , t  T, t.1, q_le(r;s), t.2, , , x f y, gset, a < b, goset, a <p b, <+>, a < b, r < s, False, x(s), S  T
Lemmas	qadd comm q, qinv inv q, bool wf, true wf, squash wf, not functionality wrt iff, assert of bnot, assert-qeq, or functionality wrt iff, assert of bor, and functionality wrt iff, assert of band, iff transitivity, iff functionality wrt iff, all functionality wrt iff, qadd wf, not wf, int inc rationals, qmul wf, bnot wf, qeq wf2, qsub wf, qpositive wf, bor wf, band wf, assert wf, iff wf, rationals wf